Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental stepin checking for possible errors in LTL assertions. Extant LTL satisfiabilitycheckers use a variety of different search procedures. With the sole exceptionof LTL satisfiability checking based on bounded model checking, which does notprovide a complete decision procedure, LTL satisfiability checkers have nottaken advantage of the remarkable progress over the past 20 years in Booleansatisfiability solving. In this paper, we propose a new LTLsatisfiability-checking framework that is accelerated using a Boolean SATsolver. Our approach is based on the variant of the \emph{obligation-setmethod}, which we proposed in earlier work. We describe here heuristics thatallow the use of a Boolean SAT solver to analyze the obligations for a givenLTL formula. The experimental evaluation indicates that the new approachprovides a a significant performance advantage.
展开▼
